\begin{tabbing}
config{-}antecedent(${\it es}$;${\it Master}$;${\it Config}$;$c$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Config}$). es{-}causl(${\it es}$; ($c$($e$)); $e$))\+
\\[0ex]\& (\=$\forall$$e_{1}$:es{-}E{-}interface(${\it es}$;${\it Config}$), $e_{2}$:es{-}E{-}interface(${\it es}$;${\it Config}$).\+
\\[0ex]es{-}causl(${\it es}$; ($c$($e_{1}$)); ($c$($e_{2}$)))
\\[0ex]$\Rightarrow$ (es{-}loc(${\it es}$; $e_{1}$) = es{-}loc(${\it es}$; $e_{2}$) $\in$ Id)
\\[0ex]$\Rightarrow$ es{-}locl(${\it es}$; $e_{1}$; $e_{2}$))
\-\\[0ex]\& (\=$\forall$$e$:es{-}E{-}interface(${\it es}$;${\it Config}$).\+
\\[0ex]let \=$m$\= = ${\it Master}$($c$($e$)) in\+\+
\\[0ex]chain\_config\_ind(${\it Config}$($e$);($\uparrow$cmconfig?($m$))
\-\\[0ex]\& ($\parallel$cmconfig{-}list($m$)$\parallel$ $\geq$ 1 )
\\[0ex]\& es{-}loc(${\it es}$; $e$) = hd(cmconfig{-}list($m$)) $\in$ Id;($\uparrow$cmconfig?($m$))
\\[0ex]\& ($\neg$($\uparrow$null(cmconfig{-}list($m$))))
\\[0ex]\& es{-}loc(${\it es}$; $e$) = last(cmconfig{-}list($m$)) $\in$ Id;$i$.($\uparrow$cmconfig?($m$))
\\[0ex]\& ($\exists$\=${\it index}$:\{0..$\parallel$cmconfig{-}list($m$)$\parallel^{-}$\}\+
\\[0ex]((0 $<$ ${\it index}$)
\\[0ex]\& es{-}loc(${\it es}$; $e$) = cmconfig{-}list($m$)[${\it index}$] $\in$ Id
\\[0ex]\& $i$ = cmconfig{-}list($m$)[(${\it index}$ {-} 1)] $\in$ Id));$i$,$n$.($\uparrow$cmseq?($m$))
\-\\[0ex]\& $i$ = cmseq{-}to($m$) $\in$ Id
\\[0ex]\& es{-}loc(${\it es}$; $e$) = cmseq{-}from($m$) $\in$ Id
\\[0ex]\& $n$ = cmseq{-}num($m$) $\in$ $\mathbb{Z}$))
\-\-\-
\end{tabbing}